0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 86 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 5 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 2 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
goalC_in_g(s(T8)) → U3_g(T8, s2lA_in_ga(T8, X30))
s2lA_in_ga(s(T16), .(X64, X65)) → U1_ga(T16, X64, X65, s2lA_in_ga(T16, X65))
s2lA_in_ga(0, []) → s2lA_out_ga(0, [])
U1_ga(T16, X64, X65, s2lA_out_ga(T16, X65)) → s2lA_out_ga(s(T16), .(X64, X65))
U3_g(T8, s2lA_out_ga(T8, X30)) → goalC_out_g(s(T8))
goalC_in_g(s(T8)) → U4_g(T8, s2lA_in_ga(T8, T22))
U4_g(T8, s2lA_out_ga(T8, T22)) → U5_g(T8, appendB_in_gaa(T22, X97, X98))
appendB_in_gaa([], X112, X112) → appendB_out_gaa([], X112, X112)
appendB_in_gaa(.(T27, T29), X129, .(T27, X130)) → U2_gaa(T27, T29, X129, X130, appendB_in_gaa(T29, X129, X130))
U2_gaa(T27, T29, X129, X130, appendB_out_gaa(T29, X129, X130)) → appendB_out_gaa(.(T27, T29), X129, .(T27, X130))
U5_g(T8, appendB_out_gaa(T22, X97, X98)) → goalC_out_g(s(T8))
goalC_in_g(0) → goalC_out_g(0)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
goalC_in_g(s(T8)) → U3_g(T8, s2lA_in_ga(T8, X30))
s2lA_in_ga(s(T16), .(X64, X65)) → U1_ga(T16, X64, X65, s2lA_in_ga(T16, X65))
s2lA_in_ga(0, []) → s2lA_out_ga(0, [])
U1_ga(T16, X64, X65, s2lA_out_ga(T16, X65)) → s2lA_out_ga(s(T16), .(X64, X65))
U3_g(T8, s2lA_out_ga(T8, X30)) → goalC_out_g(s(T8))
goalC_in_g(s(T8)) → U4_g(T8, s2lA_in_ga(T8, T22))
U4_g(T8, s2lA_out_ga(T8, T22)) → U5_g(T8, appendB_in_gaa(T22, X97, X98))
appendB_in_gaa([], X112, X112) → appendB_out_gaa([], X112, X112)
appendB_in_gaa(.(T27, T29), X129, .(T27, X130)) → U2_gaa(T27, T29, X129, X130, appendB_in_gaa(T29, X129, X130))
U2_gaa(T27, T29, X129, X130, appendB_out_gaa(T29, X129, X130)) → appendB_out_gaa(.(T27, T29), X129, .(T27, X130))
U5_g(T8, appendB_out_gaa(T22, X97, X98)) → goalC_out_g(s(T8))
goalC_in_g(0) → goalC_out_g(0)
GOALC_IN_G(s(T8)) → U3_G(T8, s2lA_in_ga(T8, X30))
GOALC_IN_G(s(T8)) → S2LA_IN_GA(T8, X30)
S2LA_IN_GA(s(T16), .(X64, X65)) → U1_GA(T16, X64, X65, s2lA_in_ga(T16, X65))
S2LA_IN_GA(s(T16), .(X64, X65)) → S2LA_IN_GA(T16, X65)
GOALC_IN_G(s(T8)) → U4_G(T8, s2lA_in_ga(T8, T22))
U4_G(T8, s2lA_out_ga(T8, T22)) → U5_G(T8, appendB_in_gaa(T22, X97, X98))
U4_G(T8, s2lA_out_ga(T8, T22)) → APPENDB_IN_GAA(T22, X97, X98)
APPENDB_IN_GAA(.(T27, T29), X129, .(T27, X130)) → U2_GAA(T27, T29, X129, X130, appendB_in_gaa(T29, X129, X130))
APPENDB_IN_GAA(.(T27, T29), X129, .(T27, X130)) → APPENDB_IN_GAA(T29, X129, X130)
goalC_in_g(s(T8)) → U3_g(T8, s2lA_in_ga(T8, X30))
s2lA_in_ga(s(T16), .(X64, X65)) → U1_ga(T16, X64, X65, s2lA_in_ga(T16, X65))
s2lA_in_ga(0, []) → s2lA_out_ga(0, [])
U1_ga(T16, X64, X65, s2lA_out_ga(T16, X65)) → s2lA_out_ga(s(T16), .(X64, X65))
U3_g(T8, s2lA_out_ga(T8, X30)) → goalC_out_g(s(T8))
goalC_in_g(s(T8)) → U4_g(T8, s2lA_in_ga(T8, T22))
U4_g(T8, s2lA_out_ga(T8, T22)) → U5_g(T8, appendB_in_gaa(T22, X97, X98))
appendB_in_gaa([], X112, X112) → appendB_out_gaa([], X112, X112)
appendB_in_gaa(.(T27, T29), X129, .(T27, X130)) → U2_gaa(T27, T29, X129, X130, appendB_in_gaa(T29, X129, X130))
U2_gaa(T27, T29, X129, X130, appendB_out_gaa(T29, X129, X130)) → appendB_out_gaa(.(T27, T29), X129, .(T27, X130))
U5_g(T8, appendB_out_gaa(T22, X97, X98)) → goalC_out_g(s(T8))
goalC_in_g(0) → goalC_out_g(0)
GOALC_IN_G(s(T8)) → U3_G(T8, s2lA_in_ga(T8, X30))
GOALC_IN_G(s(T8)) → S2LA_IN_GA(T8, X30)
S2LA_IN_GA(s(T16), .(X64, X65)) → U1_GA(T16, X64, X65, s2lA_in_ga(T16, X65))
S2LA_IN_GA(s(T16), .(X64, X65)) → S2LA_IN_GA(T16, X65)
GOALC_IN_G(s(T8)) → U4_G(T8, s2lA_in_ga(T8, T22))
U4_G(T8, s2lA_out_ga(T8, T22)) → U5_G(T8, appendB_in_gaa(T22, X97, X98))
U4_G(T8, s2lA_out_ga(T8, T22)) → APPENDB_IN_GAA(T22, X97, X98)
APPENDB_IN_GAA(.(T27, T29), X129, .(T27, X130)) → U2_GAA(T27, T29, X129, X130, appendB_in_gaa(T29, X129, X130))
APPENDB_IN_GAA(.(T27, T29), X129, .(T27, X130)) → APPENDB_IN_GAA(T29, X129, X130)
goalC_in_g(s(T8)) → U3_g(T8, s2lA_in_ga(T8, X30))
s2lA_in_ga(s(T16), .(X64, X65)) → U1_ga(T16, X64, X65, s2lA_in_ga(T16, X65))
s2lA_in_ga(0, []) → s2lA_out_ga(0, [])
U1_ga(T16, X64, X65, s2lA_out_ga(T16, X65)) → s2lA_out_ga(s(T16), .(X64, X65))
U3_g(T8, s2lA_out_ga(T8, X30)) → goalC_out_g(s(T8))
goalC_in_g(s(T8)) → U4_g(T8, s2lA_in_ga(T8, T22))
U4_g(T8, s2lA_out_ga(T8, T22)) → U5_g(T8, appendB_in_gaa(T22, X97, X98))
appendB_in_gaa([], X112, X112) → appendB_out_gaa([], X112, X112)
appendB_in_gaa(.(T27, T29), X129, .(T27, X130)) → U2_gaa(T27, T29, X129, X130, appendB_in_gaa(T29, X129, X130))
U2_gaa(T27, T29, X129, X130, appendB_out_gaa(T29, X129, X130)) → appendB_out_gaa(.(T27, T29), X129, .(T27, X130))
U5_g(T8, appendB_out_gaa(T22, X97, X98)) → goalC_out_g(s(T8))
goalC_in_g(0) → goalC_out_g(0)
APPENDB_IN_GAA(.(T27, T29), X129, .(T27, X130)) → APPENDB_IN_GAA(T29, X129, X130)
goalC_in_g(s(T8)) → U3_g(T8, s2lA_in_ga(T8, X30))
s2lA_in_ga(s(T16), .(X64, X65)) → U1_ga(T16, X64, X65, s2lA_in_ga(T16, X65))
s2lA_in_ga(0, []) → s2lA_out_ga(0, [])
U1_ga(T16, X64, X65, s2lA_out_ga(T16, X65)) → s2lA_out_ga(s(T16), .(X64, X65))
U3_g(T8, s2lA_out_ga(T8, X30)) → goalC_out_g(s(T8))
goalC_in_g(s(T8)) → U4_g(T8, s2lA_in_ga(T8, T22))
U4_g(T8, s2lA_out_ga(T8, T22)) → U5_g(T8, appendB_in_gaa(T22, X97, X98))
appendB_in_gaa([], X112, X112) → appendB_out_gaa([], X112, X112)
appendB_in_gaa(.(T27, T29), X129, .(T27, X130)) → U2_gaa(T27, T29, X129, X130, appendB_in_gaa(T29, X129, X130))
U2_gaa(T27, T29, X129, X130, appendB_out_gaa(T29, X129, X130)) → appendB_out_gaa(.(T27, T29), X129, .(T27, X130))
U5_g(T8, appendB_out_gaa(T22, X97, X98)) → goalC_out_g(s(T8))
goalC_in_g(0) → goalC_out_g(0)
APPENDB_IN_GAA(.(T27, T29), X129, .(T27, X130)) → APPENDB_IN_GAA(T29, X129, X130)
APPENDB_IN_GAA(.(T29)) → APPENDB_IN_GAA(T29)
From the DPs we obtained the following set of size-change graphs:
S2LA_IN_GA(s(T16), .(X64, X65)) → S2LA_IN_GA(T16, X65)
goalC_in_g(s(T8)) → U3_g(T8, s2lA_in_ga(T8, X30))
s2lA_in_ga(s(T16), .(X64, X65)) → U1_ga(T16, X64, X65, s2lA_in_ga(T16, X65))
s2lA_in_ga(0, []) → s2lA_out_ga(0, [])
U1_ga(T16, X64, X65, s2lA_out_ga(T16, X65)) → s2lA_out_ga(s(T16), .(X64, X65))
U3_g(T8, s2lA_out_ga(T8, X30)) → goalC_out_g(s(T8))
goalC_in_g(s(T8)) → U4_g(T8, s2lA_in_ga(T8, T22))
U4_g(T8, s2lA_out_ga(T8, T22)) → U5_g(T8, appendB_in_gaa(T22, X97, X98))
appendB_in_gaa([], X112, X112) → appendB_out_gaa([], X112, X112)
appendB_in_gaa(.(T27, T29), X129, .(T27, X130)) → U2_gaa(T27, T29, X129, X130, appendB_in_gaa(T29, X129, X130))
U2_gaa(T27, T29, X129, X130, appendB_out_gaa(T29, X129, X130)) → appendB_out_gaa(.(T27, T29), X129, .(T27, X130))
U5_g(T8, appendB_out_gaa(T22, X97, X98)) → goalC_out_g(s(T8))
goalC_in_g(0) → goalC_out_g(0)
S2LA_IN_GA(s(T16), .(X64, X65)) → S2LA_IN_GA(T16, X65)
S2LA_IN_GA(s(T16)) → S2LA_IN_GA(T16)
From the DPs we obtained the following set of size-change graphs: